The present invention generally relates to the field of formal verification for circuit designs in circuit simulation software. More specifically, the present invention relates to guiding formal verification while verifying behavior of circuit designs.
Over the last few years, the complexity of integrated circuits has increased greatly. This increase in complexity has exacerbated the difficulty of verifying circuit designs. In a typical integrated circuit design process, which includes many steps, the verification step consumes approximately 70–80% of the total time and resources. As a result, for a circuit design, aspects such as time-to-market, profit margins, etc. greatly depend on the verification step. Flaws in the design that are not found during the verification step have significant economic impact in terms of increased time-to-market and reduced profit margins. Thus, to maximize profit, the technique used for verification needs to be highly efficient.
Traditionally, simulation-based techniques have been used to verify design correctness. In the early 1970s, verification and debugging techniques based on transistor circuit-level simulation were used. Circuit-level simulation evolved to logic gate level simulation in the late 1980s. Presently, Register Transfer Level (RTL)-level simulation is used to verify circuit designs. RTL is a hardware description language (HDL) used in describing registers of a digital electronic system, and the way in which data is transferred between them.
The simulation process uses RTL source code and a “Test Bench” to verify a design. The Test Bench contains a subset of all possible inputs to the circuit/logic. For an ‘n’ input circuit, there are 2n possible inputs at any given time. For large n, e.g., for a complex design, the number of possible input sequences becomes prohibitively large. To simplify this, only a subset of all possible inputs is described in any given Test Bench.
As the complexity of designs increased with the passage of time, drawbacks associated with simulation-based techniques came into light. These simulation based techniques became less effective because of the following drawbacks: 1) the requirement of a large amount of time to verify circuit designs, 2) the employment of a huge amount of resources due and thus large costs and 3) the inability to completely and quickly verify large designs. For large and complex designs, where large combinations of inputs are possible, the simulation process is not reliable. This is due to the fact that the simulation process verifies the circuit only for a subset of inputs described in the Test Bench. Thus, circuit behavior for all possible combinations of inputs is not checked by the simulation process.
To overcome the drawbacks associated with simulation-based techniques, a new technique, called Formal Verification, was introduced. Formal verification makes use of RTL source code and constraints (also called requirements or properties) to verify circuit designs. Here, constraints refer to design constraints, i.e. specifications to be satisfied by the circuit designs. The specifications are defined in pure mathematical terms using intensive mathematical properties. In other words, formal verification methods model circuit behavior in mathematical terms and verify design constraints using exact calculations.
Formal verification methods are more exhaustive when compared to simulation methods as they utilize intensive mathematical calculations to verify circuit designs. The use of intensive mathematical calculations results in generation of all possible valid inputs for a given circuit and is akin to exhaustive simulation, i.e. testing the circuit for all possible inputs. Formal Verification methods provide the following advantages over the simulation methods—1) reduced validation time and thus less time-to-market, 2) reduced costs, and 3) high reliability and thus application in safety critical applications like air-bag deployment systems, public-transport systems, etc.
Typical formal verification methods make use of the following approaches to verify circuit designs:
Automatic test pattern generation (ATPG) is used to generate test patterns for the circuit design to be checked. The ATPG test patterns are validated against the design. Any discrepancies between the ATPG test patterns' expected value and the simulation value implies an error in the design. This error is fixed by modifying the design.
Boolean decision diagram (BDD) based symbolic model checking is the most widely used technology for formal verification. BDD is a technique for representing logic functions that is well known in the art. A description of the techniques used to create and manipulate BDDs may be found in R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 677–691.
The use of symbolic model checking is restricted to designs that contain a couple of hundreds of sequential cells (flops or latches). This makes it impossible to use this approach to verify large and complex real-world designs.
Apart from abovementioned approaches, there are various approaches that are used for formal verification.
One such approach is described in a paper by Dong Wang et. al. from Carnegie Mellon University, Design Automation Conference (DAC) 2001. This paper is titled “Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines”. The Formal verification technique provided in this paper is based on abstraction refinement strategy. Initially a simple abstract model of the circuit design is generated. In the abstract model, either the property of the design to be verified is proved or a counterexample is identified. The abstract model is refined incrementally and fully automatically using abstraction refinement until the underlying formal verification engine verifies or does not verify (falsifies) the design.
The abovementioned approaches suffer from one or more of the following disadvantages. In case, there is an error in the design, an excessive amount of time is spent in identifying the error in the circuit design. This is generally because when a property is not true for the design, more and more registers are added to the abstract model. Thus, excessive time is spent in the analysis. In addition, these approaches aim at fully automating the process of formal verification. In the process of automation, knowledge of the circuit designer is not utilized. Thus, these approaches take a large amount time to perform verification.
In light of the drawbacks associated with the prior art systems, there is a need for a system that reduces time for verification by utilizing the knowledge of a circuit designer. Thus, in addition to automatic verification, there is a need for a system that enables the designer to manually input information for formal verification. There is a need for a system that refines the abstract model efficiently so that chances of either verifying or falsifying circuit properties are maximized. Also, there is a need for an abstraction refinement strategy that reduces time for verification.